Runtime Complexity (innermost) proof of /tmp/tmplSLaof/157388.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS

↳1 CpxTrsMatchBoundsProof (⇔)

↳2 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(1(0(1(x1)))) → 0(0(2(1(3(1(x1))))))
0(1(0(1(x1)))) → 2(1(0(2(0(1(x1))))))
0(1(0(1(x1)))) → 2(1(3(1(0(0(x1))))))
4(1(0(1(x1)))) → 1(0(4(2(1(x1)))))
4(1(0(1(x1)))) → 4(1(0(2(1(x1)))))
4(1(0(1(x1)))) → 0(2(1(3(4(1(x1))))))
4(1(0(1(x1)))) → 0(4(2(1(3(1(x1))))))
4(1(0(1(x1)))) → 1(0(2(4(1(3(x1))))))
4(1(0(1(x1)))) → 1(0(4(2(2(1(x1))))))
4(1(0(1(x1)))) → 1(0(4(5(2(1(x1))))))
4(1(0(1(x1)))) → 4(0(2(1(3(1(x1))))))
4(1(0(1(x1)))) → 4(1(0(2(1(3(x1))))))
4(1(0(1(x1)))) → 4(1(3(0(2(1(x1))))))
4(1(1(1(x1)))) → 4(1(3(1(3(1(x1))))))
4(3(0(1(x1)))) → 0(2(1(3(4(x1)))))
4(3(0(1(x1)))) → 0(2(4(1(3(x1)))))
4(3(0(1(x1)))) → 0(4(2(1(3(x1)))))
4(3(0(1(x1)))) → 3(0(4(2(1(x1)))))
4(3(0(1(x1)))) → 3(4(0(2(1(x1)))))
4(3(0(1(x1)))) → 4(0(2(1(3(x1)))))
4(3(0(1(x1)))) → 4(3(0(2(1(x1)))))
4(3(0(1(x1)))) → 0(2(1(3(3(4(x1))))))
4(3(0(1(x1)))) → 0(2(1(3(4(3(x1))))))
4(3(0(1(x1)))) → 0(2(4(1(3(3(x1))))))
4(3(0(1(x1)))) → 0(4(2(2(1(3(x1))))))
4(3(0(1(x1)))) → 0(4(5(2(1(3(x1))))))
4(3(0(1(x1)))) → 1(0(2(1(3(4(x1))))))
4(3(0(1(x1)))) → 1(0(2(4(1(3(x1))))))
4(3(0(1(x1)))) → 1(0(4(2(1(3(x1))))))
4(3(0(1(x1)))) → 1(3(0(4(2(1(x1))))))
4(3(0(1(x1)))) → 3(0(4(5(2(1(x1))))))
4(3(0(1(x1)))) → 3(1(0(4(2(1(x1))))))
4(3(0(1(x1)))) → 3(3(4(0(2(1(x1))))))
4(3(0(1(x1)))) → 3(4(0(2(1(3(x1))))))
4(3(0(1(x1)))) → 3(4(0(2(2(1(x1))))))
4(3(0(1(x1)))) → 3(4(0(5(2(1(x1))))))
4(3(0(1(x1)))) → 3(4(1(0(2(1(x1))))))
4(3(0(1(x1)))) → 3(4(3(0(2(1(x1))))))
4(3(0(1(x1)))) → 4(3(0(2(1(3(x1))))))
4(3(0(1(x1)))) → 4(3(0(5(2(1(x1))))))
4(3(0(1(x1)))) → 4(3(1(0(2(1(x1))))))
4(3(0(1(x1)))) → 4(3(3(0(2(1(x1))))))
4(5(1(1(x1)))) → 4(5(2(1(1(x1)))))
4(5(1(1(x1)))) → 4(2(5(2(1(1(x1))))))
4(5(1(1(x1)))) → 4(5(2(1(3(1(x1))))))
4(5(1(1(x1)))) → 4(5(2(2(1(1(x1))))))
4(5(1(1(x1)))) → 4(5(5(2(1(1(x1))))))
0(0(1(0(1(x1))))) → 0(0(1(0(2(1(x1))))))
0(0(3(1(1(x1))))) → 2(1(3(1(0(0(x1))))))
0(0(5(1(1(x1))))) → 5(0(0(2(1(1(x1))))))
0(4(1(0(1(x1))))) → 2(1(0(4(0(1(x1))))))
0(4(3(0(1(x1))))) → 0(0(2(1(3(4(x1))))))
0(4(3(0(1(x1))))) → 0(4(3(0(2(1(x1))))))
0(4(3(0(1(x1))))) → 2(3(1(0(4(0(x1))))))
0(4(3(1(1(x1))))) → 2(1(4(1(3(0(x1))))))
0(4(3(1(1(x1))))) → 4(2(0(3(1(1(x1))))))
0(4(5(1(1(x1))))) → 4(0(1(5(2(1(x1))))))
0(4(5(1(1(x1))))) → 5(2(1(4(0(1(x1))))))
4(0(3(0(1(x1))))) → 0(0(4(2(1(3(x1))))))
4(0(3(0(1(x1))))) → 2(0(4(0(1(3(x1))))))
4(0(3(0(1(x1))))) → 2(0(4(0(3(1(x1))))))
4(1(0(1(1(x1))))) → 1(0(4(2(1(1(x1))))))
4(1(1(0(1(x1))))) → 4(1(0(2(1(1(x1))))))
4(1(2(0(1(x1))))) → 0(4(2(1(3(1(x1))))))
4(1(2(0(1(x1))))) → 1(0(2(4(1(3(x1))))))
4(1(2(0(1(x1))))) → 4(0(2(2(1(1(x1))))))
4(1(2(0(1(x1))))) → 4(1(0(2(2(1(x1))))))
4(1(3(0(1(x1))))) → 4(1(3(0(2(1(x1))))))
4(1(5(0(1(x1))))) → 1(1(5(0(4(2(x1))))))
4(1(5(1(1(x1))))) → 1(4(5(2(1(1(x1))))))
4(3(0(1(1(x1))))) → 1(3(0(2(1(4(x1))))))
4(3(0(1(1(x1))))) → 1(3(1(4(0(2(x1))))))
4(3(0(1(1(x1))))) → 1(3(1(4(2(0(x1))))))
4(3(0(1(1(x1))))) → 3(1(0(2(4(1(x1))))))
4(3(0(1(1(x1))))) → 4(3(1(1(0(2(x1))))))
4(3(1(0(1(x1))))) → 0(4(2(1(3(1(x1))))))
4(3(1(0(1(x1))))) → 1(3(4(0(2(1(x1))))))
4(3(2(0(1(x1))))) → 3(4(0(2(2(1(x1))))))
4(3(2(0(1(x1))))) → 3(4(0(5(2(1(x1))))))
4(3(2(0(1(x1))))) → 4(0(2(1(3(1(x1))))))
4(3(2(0(1(x1))))) → 4(3(0(2(1(3(x1))))))
4(3(2(1(1(x1))))) → 1(3(1(2(4(2(x1))))))
4(3(2(1(1(x1))))) → 1(3(1(4(5(2(x1))))))
4(3(2(1(1(x1))))) → 3(1(3(4(1(2(x1))))))
4(3(2(1(1(x1))))) → 4(1(3(1(2(2(x1))))))
4(3(2(1(1(x1))))) → 4(1(3(3(1(2(x1))))))
4(3(3(0(1(x1))))) → 4(3(3(0(2(1(x1))))))
4(3(4(0(1(x1))))) → 3(4(0(4(2(1(x1))))))
4(3(4(0(1(x1))))) → 4(4(0(2(1(3(x1))))))
4(3(5(0(1(x1))))) → 0(5(2(3(1(4(x1))))))
4(3(5(0(1(x1))))) → 1(3(0(2(5(4(x1))))))
4(3(5(0(1(x1))))) → 1(3(0(4(2(5(x1))))))
4(3(5(0(1(x1))))) → 1(3(4(0(5(2(x1))))))
4(3(5(0(1(x1))))) → 3(1(0(4(2(5(x1))))))
4(3(5(0(1(x1))))) → 3(1(5(0(4(2(x1))))))
4(3(5(0(1(x1))))) → 3(4(0(2(1(5(x1))))))
4(3(5(0(1(x1))))) → 3(4(1(5(0(2(x1))))))
4(3(5(0(1(x1))))) → 3(5(1(0(4(2(x1))))))
4(3(5(0(1(x1))))) → 4(3(0(2(1(5(x1))))))
4(3(5(0(1(x1))))) → 5(1(3(4(0(2(x1))))))
4(3(5(1(1(x1))))) → 1(4(5(2(1(3(x1))))))
4(3(5(1(1(x1))))) → 3(1(1(5(4(2(x1))))))
4(3(5(1(1(x1))))) → 3(1(4(5(2(1(x1))))))
4(3(5(1(1(x1))))) → 4(1(3(1(3(5(x1))))))
4(3(5(1(1(x1))))) → 4(1(5(2(1(3(x1))))))
4(3(5(1(1(x1))))) → 4(3(1(5(2(1(x1))))))
4(4(1(0(1(x1))))) → 4(4(1(0(2(1(x1))))))
4(4(3(0(1(x1))))) → 0(4(4(2(1(3(x1))))))
4(4(3(0(1(x1))))) → 4(0(2(1(3(4(x1))))))
4(4(3(0(1(x1))))) → 4(3(4(0(2(1(x1))))))
4(4(3(0(1(x1))))) → 4(4(3(0(2(1(x1))))))
4(5(1(0(1(x1))))) → 0(5(1(3(4(1(x1))))))
4(5(1(0(1(x1))))) → 0(5(4(1(3(1(x1))))))
4(5(1(0(1(x1))))) → 1(0(4(5(2(1(x1))))))
4(5(1(0(1(x1))))) → 4(0(5(2(1(1(x1))))))
4(5(1(0(1(x1))))) → 4(5(1(0(2(1(x1))))))
4(5(1(0(1(x1))))) → 5(1(0(2(4(1(x1))))))
4(5(1(0(1(x1))))) → 5(4(1(0(2(1(x1))))))
4(5(1(1(1(x1))))) → 4(5(2(1(1(1(x1))))))
4(5(3(0(1(x1))))) → 0(2(1(3(4(5(x1))))))
4(5(3(0(1(x1))))) → 0(5(2(1(3(4(x1))))))
4(5(3(0(1(x1))))) → 0(5(2(4(3(1(x1))))))
4(5(3(0(1(x1))))) → 0(5(4(2(1(3(x1))))))
4(5(3(0(1(x1))))) → 1(0(5(1(3(4(x1))))))
4(5(3(0(1(x1))))) → 1(5(0(3(3(4(x1))))))
4(5(3(0(1(x1))))) → 2(1(4(5(0(3(x1))))))
4(5(3(0(1(x1))))) → 2(4(1(3(5(0(x1))))))
4(5(3(0(1(x1))))) → 3(0(4(5(2(1(x1))))))
4(5(3(0(1(x1))))) → 4(0(3(1(5(2(x1))))))
4(5(3(0(1(x1))))) → 4(0(3(3(5(1(x1))))))
4(5(3(0(1(x1))))) → 4(0(5(4(1(3(x1))))))
4(5(3(0(1(x1))))) → 4(1(3(5(0(3(x1))))))
4(5(3(0(1(x1))))) → 4(1(3(5(5(0(x1))))))
4(5(3(0(1(x1))))) → 4(2(5(0(3(1(x1))))))
4(5(3(0(1(x1))))) → 4(5(2(0(3(1(x1))))))
4(5(3(0(1(x1))))) → 5(0(3(1(4(1(x1))))))
4(5(3(0(1(x1))))) → 5(0(3(4(4(1(x1))))))
4(5(3(0(1(x1))))) → 5(1(3(0(3(4(x1))))))
4(5(3(0(1(x1))))) → 5(2(1(3(4(0(x1))))))
4(5(3(0(1(x1))))) → 5(2(4(1(3(0(x1))))))
4(5(3(0(1(x1))))) → 5(3(0(4(2(1(x1))))))
4(5(3(0(1(x1))))) → 5(4(1(3(0(1(x1))))))
4(5(3(0(1(x1))))) → 5(4(1(3(2(0(x1))))))
4(5(3(0(1(x1))))) → 5(4(3(0(2(1(x1))))))
4(5(3(1(1(x1))))) → 2(4(1(3(1(5(x1))))))
4(5(3(1(1(x1))))) → 4(5(2(1(3(1(x1))))))
4(5(3(1(1(x1))))) → 5(1(3(4(1(2(x1))))))
4(5(3(1(1(x1))))) → 5(2(1(4(1(3(x1))))))
4(5(3(1(1(x1))))) → 5(4(2(1(3(1(x1))))))
4(5(5(1(1(x1))))) → 5(5(2(1(1(4(x1))))))
4(5(5(1(1(x1))))) → 5(5(2(4(1(1(x1))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.

Start state: 11009
Accept states: [11010, 11011]
Transitions:
11009→11010[0_1|0]
11009→11011[4_1|0]
11009→11009[1_1|0, 2_1|0, 3_1|0, 5_1|0]
11009→11012[1_1|1]
11009→11017[1_1|1]
11009→11022[1_1|1]
11009→11026[1_1|1]
11009→11031[1_1|1]
11009→11036[1_1|1]
11009→11041[1_1|1]
11009→11046[1_1|1]
11009→11051[3_1|1]
11009→11056[2_1|1]
11009→11061[1_1|1]
11009→11066[5_1|1]
11009→11071[3_1|1]
11009→11076[1_1|1]
11009→11081[4_1|1]
11009→11086[1_1|1]
11009→11091[5_1|1]
11009→11096[2_1|1]
11009→11101[3_1|1]
11009→11106[1_1|1]
11009→11111[2_1|1]
11009→11116[2_1|1]
11009→11121[2_1|1]
11009→11126[2_1|1]
11009→11131[2_1|1]
11012→11013[3_1|1]
11013→11014[1_1|1]
11014→11015[3_1|1]
11015→11016[1_1|1]
11016→11011[4_1|1]
11016→11081[4_1|1]
11016→11088[4_1|1]
11017→11018[1_1|1]
11018→11019[1_1|1]
11019→11020[2_1|1]
11020→11021[5_1|1]
11021→11011[4_1|1]
11021→11081[4_1|1]
11022→11023[1_1|1]
11023→11024[2_1|1]
11024→11025[5_1|1]
11025→11011[4_1|1]
11025→11081[4_1|1]
11026→11027[1_1|1]
11027→11028[2_1|1]
11028→11029[5_1|1]
11029→11030[2_1|1]
11030→11011[4_1|1]
11030→11081[4_1|1]
11031→11032[3_1|1]
11032→11033[1_1|1]
11033→11034[2_1|1]
11034→11035[5_1|1]
11035→11011[4_1|1]
11035→11081[4_1|1]
11036→11037[1_1|1]
11037→11038[2_1|1]
11038→11039[2_1|1]
11039→11040[5_1|1]
11040→11011[4_1|1]
11040→11081[4_1|1]
11041→11042[1_1|1]
11042→11043[2_1|1]
11043→11044[5_1|1]
11044→11045[5_1|1]
11045→11011[4_1|1]
11045→11081[4_1|1]
11046→11047[1_1|1]
11047→11048[2_1|1]
11048→11049[5_1|1]
11049→11050[4_1|1]
11050→11011[1_1|1]
11050→11081[1_1|1]
11051→11052[1_1|1]
11052→11053[2_1|1]
11053→11054[5_1|1]
11054→11055[4_1|1]
11055→11011[1_1|1]
11055→11081[1_1|1]
11056→11057[4_1|1]
11057→11058[5_1|1]
11058→11059[1_1|1]
11059→11060[1_1|1]
11060→11011[3_1|1]
11060→11081[3_1|1]
11061→11062[2_1|1]
11062→11063[5_1|1]
11063→11064[4_1|1]
11064→11065[1_1|1]
11065→11011[3_1|1]
11065→11081[3_1|1]
11066→11067[3_1|1]
11067→11068[1_1|1]
11068→11069[3_1|1]
11069→11070[1_1|1]
11070→11011[4_1|1]
11070→11081[4_1|1]
11071→11072[1_1|1]
11072→11073[2_1|1]
11073→11074[5_1|1]
11074→11075[1_1|1]
11075→11011[4_1|1]
11075→11081[4_1|1]
11076→11077[2_1|1]
11077→11078[5_1|1]
11078→11079[1_1|1]
11079→11080[3_1|1]
11080→11011[4_1|1]
11080→11081[4_1|1]
11081→11082[1_1|1]
11082→11083[1_1|1]
11083→11084[2_1|1]
11084→11085[5_1|1]
11085→11011[5_1|1]
11085→11081[5_1|1]
11086→11087[1_1|1]
11087→11088[4_1|1]
11088→11089[2_1|1]
11089→11090[5_1|1]
11090→11011[5_1|1]
11090→11081[5_1|1]
11091→11092[1_1|1]
11092→11093[3_1|1]
11093→11094[1_1|1]
11094→11095[4_1|1]
11095→11011[2_1|1]
11095→11081[2_1|1]
11096→11097[1_1|1]
11097→11098[4_1|1]
11098→11099[3_1|1]
11099→11100[1_1|1]
11100→11011[5_1|1]
11100→11081[5_1|1]
11101→11102[1_1|1]
11102→11103[4_1|1]
11103→11104[1_1|1]
11104→11105[2_1|1]
11105→11011[5_1|1]
11105→11081[5_1|1]
11106→11107[3_1|1]
11107→11108[1_1|1]
11108→11109[2_1|1]
11109→11110[4_1|1]
11110→11011[5_1|1]
11110→11081[5_1|1]
11111→11112[4_1|1]
11112→11113[2_1|1]
11113→11114[1_1|1]
11114→11115[3_1|1]
11115→11011[1_1|1]
11115→11081[1_1|1]
11116→11117[5_1|1]
11117→11118[4_1|1]
11118→11119[1_1|1]
11119→11120[3_1|1]
11120→11011[1_1|1]
11120→11081[1_1|1]
11121→11122[1_1|1]
11122→11123[4_1|1]
11123→11124[3_1|1]
11124→11125[1_1|1]
11125→11011[3_1|1]
11125→11081[3_1|1]
11126→11127[2_1|1]
11127→11128[1_1|1]
11128→11129[3_1|1]
11129→11130[1_1|1]
11130→11011[4_1|1]
11130→11081[4_1|1]
11131→11132[1_1|1]
11132→11133[3_1|1]
11133→11134[3_1|1]
11134→11135[1_1|1]
11135→11011[4_1|1]
11135→11081[4_1|1]

(0) Obligation:

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

(2) BOUNDS(O(1), O(n^1))